lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

Logical foundations of mathematics.md (2004B)

      1 +++
      2 title = 'Logical foundations of mathematics'
      3 +++
      4 # Logical foundations of mathematics
      5 ## Universes
      6 Girard's paradox: Type : Type ⇒ false
      7 Russel's paradox: {x | x ∈ x }
      8 
      9 Types have a type.
     10 You can't type Type as Type because of Girard's paradox.
     11 
     12 So you set up something like this:
     13 - `Prop`: Sort 0
     14 - `Type`: Sort 1
     15 - `Type 1`: Sort 2
     16 - etc.
     17 
     18 The types of types are "universes".
     19 `u` in `Sort u` is "universe level".
     20 
     21 ## The Prop universe
     22 `Prop` is different from other universes.
     23 
     24 ### Universe of α → β (impredicativity)
     25 functions are used both returning Types and returning Prop.
     26 
     27 You can use the typing rule
     28 
     29     C ⊢ σ : Sort u    C, x : σ ⊢ τ[x] : Sort v
     30     ——————————————————————————————————————————— Forall
     31     C ⊢ (∀x : σ, τ[x]) : Sort (imax u v)
     32 
     33 where
     34 
     35     imax u 0       = 0
     36     imax u (v + 1) = max u (v + 1) -/
     37 
     38 ### Proof irrelevance
     39 `∀(a : Prop) (h₁ h₂ : a), h₁ = h₂`
     40 
     41 When seeing proposition as type, and proof as element of that type, a proposition is either empty type or has exactly one inhabitant.
     42 
     43 ### No large elimination
     44 Can't extract data from a proof of a proposition.
     45 This needs to be true for proof irrelevance.
     46 
     47 ## Axiom of choice
     48 Makes it possible to get an arbitrary element from any nonempty type.
     49 `classical.choice` gives back some element of the type.
     50 It's not computable, and definitions that use it must be marked `noncomputable`.
     51 
     52 ## Subtypes
     53 If a type is a set of elements, a subtype is a subset of those elements.
     54 
     55 Given base type and property, the subtype has syntax: `{` variable `:` base type `//` property `}`
     56 So for example `{i : Ν // i ≤ n}`
     57 
     58 You create elements with `subtype.mk property proof_of_property`.
     59 
     60 ## Quotient types
     61 If a type is a set of elements, and some of those elements are equivalent, the quotient type is the set of those equivalences.
     62 You create this with a setoid (a structure with an equivalence relation and proof).